|
|
Rigid Body Simulation
Leitner, Denis ; Milet, Tomáš (referee) ; Chlubna, Tomáš (advisor)
This thesis deals with rigid body physics simulation in real time. It describes basic methods for collision detection between convex polyhedra, solving collisions and simulation of rigid body dynamics used in game development. Work also describes design and implementation of rigid body simulator written in C++ using OpenGL for rendering.
|
|
|
A Verified Data Structures Library
Rychnovský, Jan ; Holík, Lukáš (referee) ; Lengál, Ondřej (advisor)
This bachelor thesis deals with a methodology of writing verified programs using the VCC tool. The mentioned methodology is based in the principle of extending the program code with additional annotations, which provide a specification of the desired functionality. The VCC tool then uses formal methods to check whether the source code is correct with respect to the given specification. The first part describes formal verification and three basic approaches to it. Subsequently, the satisfiability problems of propositional formulae (SAT) and formulae in theories of predicate logic (SMT) are described. Then the thesis describes the VCC verification tool, its functionality, methodology, syntax and semantics of commands of its intermediate annotation language BoogiePL. The second part of this thesis is focused on the design and implementation of a verified data structures library, which contains singly linked, doubly linked, and circular lists, a binary search tree and a Treiber's stack. The text concludes with a discussion of the learnt knowledge about the programming methodology based on writing verified code.
|
|
|
Collision Detection Library
Chlubna, Tomáš ; Španěl, Michal (referee) ; Polok, Lukáš (advisor)
This thesis deals with the problem of detecting collisions of nontrivial polygonal models in three-dimensional space. In general, there are methods describing how to mathematically express and calculate such collisions. However, such methods are usually unsuitable for usage in information technology due to the performance and memory requirements. It is also necessary to work with the discrete time that is not present in the real world. That brings the need to implement algorithms that are not only able to detect the collisions in a specific point in time, but also to predict them according to the available data about the movement of the objects in the scene. The solution uses game development and physics simulations techniques. Therefore, this works describes some optimization techniques as well as suitable scene representation formats and GPU rendering mechanisms.
|
|
| |
|
|
Visualization of Tactile and Aural Sensations
Lukš, Roman ; Zachariáš, Michal (referee) ; Polok, Lukáš (advisor)
The purpose of this thesis is to design and implement visualization of aural and tactile sensations in the real-time. Sensations are to replace vision in simple 2D platform game. Visualizations are implemented on GPU. Vizualization of aural sensations implement computationally lightweight explicit method. Vizualization of tactile sensations are implemented as the animated lines. OpenGL is used to draw graphic output. Functional game prototype with vizualization of these two sensations is the output of this thesis.
|
|
|
Application of SAT Solvers in Circuit Optimization Problem
Minařík, Vojtěch ; Mrázek, Vojtěch (referee) ; Vašíček, Zdeněk (advisor)
This thesis is focused on the task of application of SAT problem and it's modifications in area of evolution logic circuit development. This task is supposed to increase speed of evaluating candidate circuits by fitness function in cases where simulation usage fails. Usage of SAT and #SAT problems make evolution of complex circuits with high input number significantly faster. Implemented solution is based on #SAT problem. Two applications were implemented. They differ by the approach to checking outputs of circuit for wrong values. Time complexity of implemented algorithm depends on logical complexity of circuit, because it uses logical formulas and it's satisfiability to evaluate logic circuits.
|
|
|
GPU Accelerated SAT Solver
Izrael, Petr ; Šimek, Václav (referee) ; Jaroš, Jiří (advisor)
This thesis is concerned with design and implementation of a complete SAT solver accelerated on GPU. The achitecture of modern graphics cards is described as well as the CUDA platform and a list of common algorithms used for solving the boolean satisfiability problem (the SAT problem). The presented solution is based on the 3-SAT DC alogirthm, which belongs to the family of well-known DPLL based algorithms. This work describes problems encountered during the design and implementation. The resulting application was then analyzed and optimized. The presented solver cannot compete with state of the art solvers, but proves that it can be up to 21x faster than an equivalent sequential version. Unfortunately, the current implementation can only handle formulas of a limited size. Suggestions on further improvements are given in final sections.
|
|
|
Magnetic fields for biomedical experiments
Otýpka, Jan ; Cipín, Radoslav (referee) ; Patočka, Miroslav (advisor)
In this work deals with magnetic fields for use in biomedicine. This solution involves the choice of the correct geometric arrangement of coils for generating magnetic field with a homogeneous distribution of magnetic induction of the widest possible area. The paper compares thre traditional types of coils, solenoid, toroid and Helmholtz coil. For Helmholtz and solenoid coil and is then carried out an analysis of the magnetic flux density in the inner space. Next part is devoted to electrical resonance in the LC circuit. This is then utilized for the development of pulsed magnetic field in the Helmholtz coil. It summarizes the theoretical and practical knowledge to design and construction of resonant converters. The end is devoted to the measurement of circuit parameters and verification of theoretical knowledge.
|
|
|
Modeling of Cooperative Path Finding
Ježek, Milan ; Surynek, Pavel (advisor) ; Majerech, Vladan (referee)
In this thesis we describe new models for solving the cooperative pathfinding (cpf) with the requirement of minimal makespan and experimental comparison with current models is performed. These new models investigate the possibilities of encoding the cpf problem into binary integer programming (bip) or constraint satisfaction problem (csp). Mainly the new active-edges IP model tests with high number of agents yielded good results, where it fell only slightly behind the best SAT model. A new csp model reached the fastest times in tests with low number of obstacles and agent interactions while struggling heavily in the opposite cases. Powered by TCPDF (www.tcpdf.org)
|
|
|
DPLL algorithm and propositional proofs
Hrnčiar, Maroš ; Krajíček, Jan (advisor) ; Koucký, Michal (referee)
Proof complexity is an interesting mathematical part connecting logic and complexity theory. It investigates which proof systems are needed for effective theorem proving. The aim of this paper is to present a relation between propositional proof systems and SAT algorithms. We will see that a run of an algorithm on the unrealizable formula can be seen as a propositional proof of its unsatisfiability, so the algorithm practically defines whole proof system. The thesis is mainly recommended for readers interested in proof complexity, but it can also independently illustrate a resolution principle and perhaps show some less common view of SAT assuming reader's basic knowledge of propositional logic, graph theory and complexity.
|
guest ::
